Termination of the given ITRSProblem could successfully be proven:



ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

Cond_b14(TRUE, sv14_14, sv23_37, sv24_38) → b15(sv14_14, sv23_37, sv24_38)
b15(sv14_14, sv23_37, sv24_38) → b10(sv14_14, -@z(sv23_37, sv14_14), +@z(sv24_38, 1@z))
b10(sv14_14, sv23_37, sv24_38) → b14(sv14_14, sv23_37, sv24_38)
b14(sv14_14, sv23_37, sv24_38) → Cond_b14(&&(>=@z(sv23_37, sv14_14), <@z(1@z, sv14_14)), sv14_14, sv23_37, sv24_38)

The set Q consists of the following terms:

Cond_b14(TRUE, x0, x1, x2)
b15(x0, x1, x2)
b10(x0, x1, x2)
b14(x0, x1, x2)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

Cond_b14(TRUE, sv14_14, sv23_37, sv24_38) → b15(sv14_14, sv23_37, sv24_38)
b15(sv14_14, sv23_37, sv24_38) → b10(sv14_14, -@z(sv23_37, sv14_14), +@z(sv24_38, 1@z))
b10(sv14_14, sv23_37, sv24_38) → b14(sv14_14, sv23_37, sv24_38)
b14(sv14_14, sv23_37, sv24_38) → Cond_b14(&&(>=@z(sv23_37, sv14_14), <@z(1@z, sv14_14)), sv14_14, sv23_37, sv24_38)

The integer pair graph contains the following rules and edges:

(0): B10(sv14_14[0], sv23_37[0], sv24_38[0]) → B14(sv14_14[0], sv23_37[0], sv24_38[0])
(1): COND_B14(TRUE, sv14_14[1], sv23_37[1], sv24_38[1]) → B15(sv14_14[1], sv23_37[1], sv24_38[1])
(2): B15(sv14_14[2], sv23_37[2], sv24_38[2]) → B10(sv14_14[2], -@z(sv23_37[2], sv14_14[2]), +@z(sv24_38[2], 1@z))
(3): B14(sv14_14[3], sv23_37[3], sv24_38[3]) → COND_B14(&&(>=@z(sv23_37[3], sv14_14[3]), <@z(1@z, sv14_14[3])), sv14_14[3], sv23_37[3], sv24_38[3])

(0) -> (3), if ((sv23_37[0]* sv23_37[3])∧(sv24_38[0]* sv24_38[3])∧(sv14_14[0]* sv14_14[3]))


(1) -> (2), if ((sv23_37[1]* sv23_37[2])∧(sv24_38[1]* sv24_38[2])∧(sv14_14[1]* sv14_14[2]))


(2) -> (0), if ((-@z(sv23_37[2], sv14_14[2]) →* sv23_37[0])∧(+@z(sv24_38[2], 1@z) →* sv24_38[0])∧(sv14_14[2]* sv14_14[0]))


(3) -> (1), if ((sv24_38[3]* sv24_38[1])∧(sv14_14[3]* sv14_14[1])∧(sv23_37[3]* sv23_37[1])∧(&&(>=@z(sv23_37[3], sv14_14[3]), <@z(1@z, sv14_14[3])) →* TRUE))



The set Q consists of the following terms:

Cond_b14(TRUE, x0, x1, x2)
b15(x0, x1, x2)
b10(x0, x1, x2)
b14(x0, x1, x2)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
IDP
          ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): B10(sv14_14[0], sv23_37[0], sv24_38[0]) → B14(sv14_14[0], sv23_37[0], sv24_38[0])
(1): COND_B14(TRUE, sv14_14[1], sv23_37[1], sv24_38[1]) → B15(sv14_14[1], sv23_37[1], sv24_38[1])
(2): B15(sv14_14[2], sv23_37[2], sv24_38[2]) → B10(sv14_14[2], -@z(sv23_37[2], sv14_14[2]), +@z(sv24_38[2], 1@z))
(3): B14(sv14_14[3], sv23_37[3], sv24_38[3]) → COND_B14(&&(>=@z(sv23_37[3], sv14_14[3]), <@z(1@z, sv14_14[3])), sv14_14[3], sv23_37[3], sv24_38[3])

(0) -> (3), if ((sv23_37[0]* sv23_37[3])∧(sv24_38[0]* sv24_38[3])∧(sv14_14[0]* sv14_14[3]))


(1) -> (2), if ((sv23_37[1]* sv23_37[2])∧(sv24_38[1]* sv24_38[2])∧(sv14_14[1]* sv14_14[2]))


(2) -> (0), if ((-@z(sv23_37[2], sv14_14[2]) →* sv23_37[0])∧(+@z(sv24_38[2], 1@z) →* sv24_38[0])∧(sv14_14[2]* sv14_14[0]))


(3) -> (1), if ((sv24_38[3]* sv24_38[1])∧(sv14_14[3]* sv14_14[1])∧(sv23_37[3]* sv23_37[1])∧(&&(>=@z(sv23_37[3], sv14_14[3]), <@z(1@z, sv14_14[3])) →* TRUE))



The set Q consists of the following terms:

Cond_b14(TRUE, x0, x1, x2)
b15(x0, x1, x2)
b10(x0, x1, x2)
b14(x0, x1, x2)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair B10(sv14_14, sv23_37, sv24_38) → B14(sv14_14, sv23_37, sv24_38) the following chains were created:




For Pair COND_B14(TRUE, sv14_14, sv23_37, sv24_38) → B15(sv14_14, sv23_37, sv24_38) the following chains were created:




For Pair B15(sv14_14, sv23_37, sv24_38) → B10(sv14_14, -@z(sv23_37, sv14_14), +@z(sv24_38, 1@z)) the following chains were created:




For Pair B14(sv14_14, sv23_37, sv24_38) → COND_B14(&&(>=@z(sv23_37, sv14_14), <@z(1@z, sv14_14)), sv14_14, sv23_37, sv24_38) the following chains were created:




To summarize, we get the following constraints P for the following pairs.



The constraints for P> respective Pbound are constructed from P where we just replace every occurence of "t ≥ s" in P by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x1, x2)) = x1 + (-1)x2   
POL(B15(x1, x2, x3)) = -1 + (2)x2 + (-1)x1   
POL(TRUE) = 1   
POL(&&(x1, x2)) = 0   
POL(FALSE) = 1   
POL(<@z(x1, x2)) = -1   
POL(COND_B14(x1, x2, x3, x4)) = -1 + (2)x3 + x2 + (-1)x1   
POL(>=@z(x1, x2)) = -1   
POL(B14(x1, x2, x3)) = -1 + (2)x2 + x1   
POL(+@z(x1, x2)) = x1 + x2   
POL(B10(x1, x2, x3)) = -1 + (2)x2 + x1   
POL(1@z) = 1   
POL(undefined) = -1   

The following pairs are in P>:

COND_B14(TRUE, sv14_14[1], sv23_37[1], sv24_38[1]) → B15(sv14_14[1], sv23_37[1], sv24_38[1])

The following pairs are in Pbound:

COND_B14(TRUE, sv14_14[1], sv23_37[1], sv24_38[1]) → B15(sv14_14[1], sv23_37[1], sv24_38[1])

The following pairs are in P:

B10(sv14_14[0], sv23_37[0], sv24_38[0]) → B14(sv14_14[0], sv23_37[0], sv24_38[0])
B15(sv14_14[2], sv23_37[2], sv24_38[2]) → B10(sv14_14[2], -@z(sv23_37[2], sv14_14[2]), +@z(sv24_38[2], 1@z))
B14(sv14_14[3], sv23_37[3], sv24_38[3]) → COND_B14(&&(>=@z(sv23_37[3], sv14_14[3]), <@z(1@z, sv14_14[3])), sv14_14[3], sv23_37[3], sv24_38[3])

At least the following rules have been oriented under context sensitive arithmetic replacement:

FALSE1&&(FALSE, FALSE)1
-@z1
+@z1
TRUE1&&(TRUE, TRUE)1
FALSE1&&(TRUE, FALSE)1
FALSE1&&(FALSE, TRUE)1


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDPNonInfProof
IDP
              ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): B10(sv14_14[0], sv23_37[0], sv24_38[0]) → B14(sv14_14[0], sv23_37[0], sv24_38[0])
(2): B15(sv14_14[2], sv23_37[2], sv24_38[2]) → B10(sv14_14[2], -@z(sv23_37[2], sv14_14[2]), +@z(sv24_38[2], 1@z))
(3): B14(sv14_14[3], sv23_37[3], sv24_38[3]) → COND_B14(&&(>=@z(sv23_37[3], sv14_14[3]), <@z(1@z, sv14_14[3])), sv14_14[3], sv23_37[3], sv24_38[3])

(0) -> (3), if ((sv23_37[0]* sv23_37[3])∧(sv24_38[0]* sv24_38[3])∧(sv14_14[0]* sv14_14[3]))


(2) -> (0), if ((-@z(sv23_37[2], sv14_14[2]) →* sv23_37[0])∧(+@z(sv24_38[2], 1@z) →* sv24_38[0])∧(sv14_14[2]* sv14_14[0]))



The set Q consists of the following terms:

Cond_b14(TRUE, x0, x1, x2)
b15(x0, x1, x2)
b10(x0, x1, x2)
b14(x0, x1, x2)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.